fix: report tech-debt changes by data-row content, not line count#45
Open
kim-em wants to merge 1 commit into
Open
fix: report tech-debt changes by data-row content, not line count#45kim-em wants to merge 1 commit into
kim-em wants to merge 1 commit into
Conversation
Previously `prSummaryReport` decided whether to render a report by
counting lines in the rendered text:
if [ "$(wc -l <<<"${rep}")" -le 5 ]; then "no changes"
That worked in the original layout (mathlib4#18971) where `report`
emitted 5 boilerplate lines (header + separator + blank + 2 commit
URLs). When the strong/weak split (#28) moved the commit URLs into a
separate `reportFooter`, only 2 boilerplate lines remained in `rep`,
but the `-le 5` threshold was kept. Any PR changing three or fewer
counters of a given level was silently reported as "no changes" — e.g.
leanprover-community/mathlib4#39932 removed
one `set_option backward.isDefEq.respectTransparency false in` without
the bot noticing.
Instead of patching the threshold (which would stay coupled to whatever
incidental formatting `report` happens to emit), filter directly to the
non-zero data rows in a named `filterChangedRows`, branch on
`[ -z "${changedRows}" ]`, and reconstruct the table header in the
"has changes" branch. The Change column is used as the test (rather
than the Current column) because a counter that disappeared entirely
in the new commit renders as `||-1|name|` — empty Current — and we
still want to report it.
🤖 Prepared with Claude Code
kim-em
force-pushed
the
fix-techdebt-threshold
branch
from
d07c443 to
347aa1d
Compare
kim-em
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes a regression introduced by #28 (the strong/weak split). That refactor moved the commit URLs out of
reportinto the newreportFooter(called separately), butprSummaryReportkept its-le 5"no changes" line-count threshold. After the split, the filtered report only carries 2 boilerplate lines (header + separator), so any PR changing three or fewer counters of a given level is silently reported as "no changes".Example: leanprover-community/mathlib4#39932 removed one
set_option backward.isDefEq.respectTransparency false in, which should have shown up as|5854|-1|backward.isDefEq.respectTransparency|, but the bot reported "No changes to strong technical debt". See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/no.20change.20to.20technical.20debt/near/598112382.Rather than patch the threshold — which would stay coupled to whatever incidental formatting
reporthappens to emit and silently rot again on the next formatting tweak — this PR filters directly to non-zero data rows (in a namedfilterChangedRows) and branches on[ -z "${changedRows}" ]. The table header is reconstructed in the "has changes" branch. The Change column is used as the emptiness test (rather than the Current column) because a counter that disappeared entirely in the new commit renders as||-1|name|— empty Current — and we still want to report it.Verified locally:
|5854|-1|backward.isDefEq.respectTransparency|.backward.inferInstanceAs.wrap.reuseSubInstancesalso reports it, as||-1|backward.inferInstanceAs.wrap.reuseSubInstances|.🤖 Prepared with Claude Code